es:ES, m:, f:({0..m}E).
(i:{0..(m - 1)}. (f(i) <loc f(i+1)))  (i:{0..m}, j:{0..(i+1)}. f(j) loc f(i) ) 

latex

Definitions	{i..j}, t  T, x:A. B(x), P  Q, Dec(P), P  Q, ES, , E, A  B, P & Q, i  j < k, False, A, (e <loc e'), , e loc e' , {T}, SQType(T)
Lemmas	es-le-self, subtype rel self, es-locl wf, le wf, int seg wf, es-E wf, nat plus wf, event system wf, es-increasing-sequence, decidable int equal